$\forall$${\it es}$:ES, $e$:E. (state when $e$) $\in$ state@loc($e$)